feat(T2): dissolve the I-ISO region-programming core — and a 40% SRAM finding - #262

… finding

Second isolation-core module onto the dissolve path after hm-thin. Unlike HM this one
HAS a seam, so it tests the part that matters.

THE SEAM SURVIVES EXACTLY.

  plain/src/mpu_switch.rs + mpu.rs (Verus+Kani verified, lifted VERBATIM)
    -> wasm 7120 B -> component 8464 B -> meld -> loom -> synth

  undefined symbols: [ mpu-write ]

One atom, exactly as declared -- nothing undeclared crept in, nothing was swallowed.
Lifted verbatim: size_field, rasr_for, RegionTable (new / program_partition /
switch_to_partition / try_add_region / covers_addr), apply_program, emit_write, plus
is_power_of_two, validate_region and MIN_REGION_SIZE from mpu.rs.

THE FOOTPRINT, AND WHY MY FIRST NUMBER WAS WRONG.

Compiled the way hm-thin was, this object reports text 3614, data 0, bss 0. True and
MISLEADING: without --native-pointer-abi the linear memory is not reserved in the
object -- the embedder supplies it -- and this module declares 17 wasm pages,
1088 KB. "Zero SRAM" would have been wrong by a factor of 136 on an 8 KB part. I
nearly recorded it, because the object's own section table supports the wrong claim.

With the shadow-stack re-base the OS-node builds already use (#383):

  shadow 2048   text 3744  data 636  bss 2688   SRAM 3324 B of 8192  = 40.6%
  shadow 1024                        bss 1664   SRAM 2300 B          = 28.1%
  shadow  512                        bss 1152   SRAM 1788 B          = 21.8%

THE CONSTRAINT THIS SURFACES: at the standard budget this ONE module takes 40.6% of
the F100's RAM. The isolation core is three modules, and a system also needs the OS
and an application. Either the budget comes down for this module or the F100 does not
host a multi-partition configuration. That belongs to the partition work, not to this
file. And the budget is ASSERTED, not proven -- the 2048-of-8192 gap already recorded.

BIN-VERIFY: 7 functions, 7 rules verified, 0 failed, 0 unknown, 20 LRAT expansions.
NOT zero-gap: 356 i32.const, skipped by BIN-VERIFY and Admitted in Rocq, so covered by
neither half -- more than ten times hm-thin's 29. synth#933 / synth#935.

NOT established: no evidence-on-wasm (no witness MC/DC, no scry, REQ-OS-ISO-001
oracles not re-run against the wasm build); nothing has executed the object; mpu_write
remains trusted native code including its barrier-pairing contract -- what moved is
the region-programming POLICY; partition_switch (3 seams) remains.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo